Inductive ByteExp : Type :=
  | byte_exp_num    : Byte      -> ByteExp
  | byte_exp_id     : Id        -> ByteExp
  | byte_exp_xor    : ByteExp   -> ByteExp  -> ByteExp
  | byte_exp_andbb  : ByteExp   -> ByteExp  -> ByteExp
  | byte_exp_shiftl : ByteExp   -> ArithExp -> ByteExp
  | byte_exp_shiftr : ByteExp   -> ArithExp -> ByteExp
  | byte_exp_matrix : MatrixExp -> ArithExp -> ArithExp -> ByteExp
.